$M$.init($x$)?$v$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}cap(1of(2of(2of($M$)));IdDeq;$x$;$v$)